$\forall$$A$, $B$:Type, $P$:($A$$\rightarrow$Prop). strong{-}subtype($A$;$B$) $\Rightarrow$ strong{-}subtype(\{$x$:$A$$\mid$ $P$($x$) \};$B$)